T:Type, R:(TTProp).
(x:T. R(x,x))
 (x, y:T. R(x,y)  R(y,x))
 (as, bs:T List.
 (l-ordered(T;x,y.R(x,y);as)
 ( l-ordered(T;x,y.R(x,y);bs)
 ( (as = bs  (x:T. (x  as)  (x  bs)))) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), l-ordered(T;x,y.R(x;y);L), x before y  l, P  Q, x(s1,s2), P & Q, P  Q, f(a), left+right, P  Q, (x  l), x:AB(x), x:AB(x), Prop, type List, s = t, no_repeats(T;l), Type, x,y. t(x;y)
Lemmas	l-ordered wf, not wf, no repeats-before-equality, l-ordered-no repeats, iff wf, l member wf, l before wf, l tricotomy, l before member, l before member2